With an increase in scale of software installed in a system, it is becoming more difficult to check all software specifications or codes through review or conduct a test thereof. In addition, in software that performs a concurrent operation, a defect may be generated due to processing timing, and there is a difficulty in detecting such a defect through a test. A method of applying model checking, which is a formal verification method, is present as a measure against the above-mentioned problem.
In model checking, a design corresponding to a checking object, specifically, software specifications or source code is expressed using a format specification descriptive language (hereinafter which will be referred to as a “verification model”). In addition, a required characteristic for the checking object is expressed as a property using a temporal logic formula which is a logic formula having a concept of time and an operator, or is expressed as an assertion by a logic formula not having a concept of time. When these verification models and a checking formula indicated by the property or the assertion are input to a model checker which is a tool operating on a computer, whether the required characteristic for the checking object is satisfied is determined by a mathematical technique such as a comprehensive state search. In addition, when the required characteristic is not satisfied, a counterexample is derived.
Meanwhile, source code is compiled and converted into object code, and is installed in a system as an executable format combined in a particular format. In this process, even when there is no defect in the source code, a defect may be generated in the object code due to an influence of optimization or a bug of a compiler. In addition, a product developer desires to verify whether defectiveness is present in the object code which is a final form of software. For this reason, application of model checking to the object code is useful when model checking is applicable to the object code. However, model checking with respect to the object code has a technical difficulty since expression of code is different according to a computer on which the object code operates, and is not common. Further, there are few tools for expression.
A technology for generating a test case by applying model checking is present as a measure against this problem. The model checker has a function of comprehensively searching for an available action or an execution path of a checking object through a verification model, and thus this function is used in a test case generation technology. A mechanism is described below.
A verification model is constructed from source code which is a source of object code set as a checking object, and a property or an assertion corresponding to “an end point of an execution path desired to be tested is not reached” is defined with respect to the end point in the source code. With regard to an input of the property or the assertion, a model checker outputs an execution path reaching the end point as a counterexample. For example, checking is executed by describing “assert (false)” at a finally executed point in the verification model using Simple Promela Interpreter (SPIN) in the model checker. When there is a case in which the point at which the assertion is described is executed, a trace corresponding to information related to an execution path from the point at which execution starts to the point at which execution ends is output as one or a plurality of counterexamples. One trace corresponds to one test case (may correspond to a plurality of test cases in which an execution condition is changed). This trace includes substitution for a variable which is non-deterministically selected in the middle, that is, input value determination or an execution order when a plurality of processes is present. This trace is converted into data for execution of a test, and is set as an input of a system in which the object code corresponding to the checking object is executed on a real machine or a simulator. This data is a test case or a part of the test case. A test case is data indicating a test condition. Herein, an expression “a part of the test case” is used since the data converted from the trace does not include a pass criterion or some execution conditions of a program set as a checking object.
This test case generation technology may include execution paths, and thus may be expected to have a similar effect to that of a technology in which model checking is performed with respect to object code. PTL 1 is present as a prior art that performs test case generation applying model checking.